app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
↳ QTRS
↳ DependencyPairsProof
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(map, app2(treemap, f))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(f, x)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(node, app2(f, x))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(app2(map, app2(treemap, f)), xs)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(map, app2(treemap, f))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(f, x)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(node, app2(f, x))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(app2(map, app2(treemap, f)), xs)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(f, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(app2(map, app2(treemap, f)), xs)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
Used ordering: Polynomial Order [17,21] with Interpretation:
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(f, x)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(app2(map, app2(treemap, f)), xs)
POL( APP2(x1, x2) ) = max{0, x2 - 2}
POL( app2(x1, x2) ) = x1 + x2 + 1
POL( cons ) = 1
POL( node ) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(f, x)
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(app2(map, app2(treemap, f)), xs)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(f, x)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP2(app2(treemap, f), app2(app2(node, x), xs)) -> APP2(f, x)
POL( APP2(x1, x2) ) = max{0, x2 - 2}
POL( app2(x1, x2) ) = x1 + x2 + 1
POL( node ) = 1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(app2(treemap, f), app2(app2(node, x), xs)) -> app2(app2(node, app2(f, x)), app2(app2(map, app2(treemap, f)), xs))